1. $i$ : $\mathbb{N}$ \\[0ex]2. $f$ : \{$f$ $\mid$ $i$:\{$z$:$\mathbb{N}\mid$ $z$ $<$ $i$\} $\rightarrow$ if ($i$ =$_{0}$ 0) then $\mathbb{Z}$ else \{$f$($i$ {-} 1)$\ldots\,$\} fi \} \\[0ex]3. $j$ : \{$k$:$\mathbb{N}\mid$ $k$ $<$ $i$\} \\[0ex]$\vdash$ $f$($j$) $\in$ $\mathbb{Z}$